#include <stdlib.h>

#include "atom.h"
#include "input.h"
#include "predicates.h"
#include "system.h"
#include "tree.h"
#include "tuple.h"

bool calculate (Node&, int&);

class CalculateSwitcher : public Switcher {
public:
  bool atom (Atom &a) {
    result = atoi (a.name.c_str ());
    return isInteger (a.name);
  }

  bool number (Number &n) {
    result = n.value;
    return true;
  }

  bool tree (Tree &t) {
    int left, right;
    if(calculate (*t.left, left) && calculate (*t.right, right))
      switch(t.ops[0]) {
      case '+':
        result = left + right;
        return true;
      case '-':
        result = left - right;
        return true;
      case '*':
        result = left * right;
        return true;
      case '/':
        result = left / right;
        return true;
      }
    return false;
  }

  bool tuple (Tuple &t) {
    int size = t.nodes.size ();

    if(size == 2) {
      Node &finalPrefixNode = *t.nodes[0].final ();
      if(finalPrefixNode.type () == Atom::ID) {
        std::string function = finalPrefixNode.dump ();
        if(function == "random" && calculate (*t.nodes[1], result)) {
          result = rand () % result;
          return true;
        } else if(function == "not" && calculate (*t.nodes[1], result)) {
          result = ~result;
          return true;
        }
      }
    }

    if(size == 3) {
      Node &finalInfixNode = *t.nodes[1].final ();
      if(finalInfixNode.type () == Atom::ID) {
        std::string function = finalInfixNode.dump ();
        int left, right;
        if(calculate (*t.nodes[0], left) && calculate (*t.nodes[2], right)) {
          if(function == "and") {
            result = left & right;
            return true;
          } else if(function == "or") {
            result = left | right;
            return true;
          } else if(function == "shl") {
            result = ((unsigned) left) << right;
            return true;
          } else if(function == "shr") {
            result = ((unsigned) left) >> right;
            return true;
          } else if(function == "mod") {
            result = left % right;
            return true;
          }
        }
      }
    }

    return false;
  }

  int result;
};

bool calculate (Node &node, int &result) {
  CalculateSwitcher switcher;
  bool ret = node.doSwitch (switcher);
  result = switcher.result;
  return ret;
}

class Less {
predicateName("<")
  bool operator () (int a, int b) {
    return a < b;
  }
};

class Greater {
predicateName(">")
  bool operator () (int a, int b) {
    return a > b;
  }
};

class LessOrEqual {
predicateName("<=")
  bool operator () (int a, int b) {
    return a <= b;
  }
};

class GreaterOrEqual {
predicateName(">=")
  bool operator () (int a, int b) {
    return a >= b;
  }
};

template <class Comparator>
class Compare : public OnceProver {
predicateName(Comparator::name ())

  bool proveOnce () {
    int left, right;
    return calculate (*tree->left, left) && calculate (*tree->right, right)
        && Comparator () (left, right);
  }

  Tree *tree;
  void set (Tree &t, System&) {
    tree = &t;
  }
};

ProverFactoryRegistrar<Compare<Less> , Tree::ID> compareLregistrar;
ProverFactoryRegistrar<Compare<Greater> , Tree::ID> compareGregistrar;
ProverFactoryRegistrar<Compare<LessOrEqual> , Tree::ID> compareLEregistrar;
ProverFactoryRegistrar<Compare<GreaterOrEqual> , Tree::ID> compareGEregistrar;

// Integer calculations
class expr : public OnceBindTupleProver {
predicateName("expr")

  bool proveOnce () {
    int result;
    if(calculate (*tuple->nodes[1], result)) {
      if(binder.bind (*tuple->nodes[2], *Number::create (result), system->trail))
        return true;
    }
    return false;
  }
};

ProverFactoryRegistrar<expr, Tuple::ID, 3> exprRegistrar;

class let : public OnceBindTupleProver {
predicateName("let")

  bool proveOnce () {
    int result;
    if(calculate (*tuple->nodes[2], result)) {
      if(binder.bind (*tuple->nodes[1], *Number::create (result), system->trail))
        return true;
    }
    return false;
  }
};

ProverFactoryRegistrar<let, Tuple::ID, 3> letRegistrar;
